Search Results

Documents authored by Scalas, Alceste

Document
DOI: 10.4230/LIPIcs.CONCUR.2022.35
Generalised Multiparty Session Types with Crash-Stop Failures

Authors: Adam D. Barwell, Alceste Scalas, Nobuko Yoshida, and Fangyi Zhou

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

Abstract
Session types enable the specification and verification of communicating systems. However, their theory often assumes that processes never fail. To address this limitation, we present a generalised multiparty session type (MPST) theory with crash-stop failures, where processes can crash arbitrarily. Our new theory validates more protocols and processes w.r.t. previous work. We apply minimal syntactic changes to standard session π-calculus and types: we model crashes and their handling semantically, with a generalised MPST typing system parametric on a behavioural safety property. We cover the spectrum between fully reliable and fully unreliable sessions, via optional reliability assumptions, and prove type safety and protocol conformance in the presence of crash-stop failures. Introducing crash-stop failures has non-trivial consequences: writing correct processes that handle all crash scenarios can be difficult. Yet, our generalised MPST theory allows us to tame this complexity, via model checking, to validate whether a multiparty session satisfies desired behavioural properties, e.g. deadlock-freedom or liveness, even in presence of crashes. We implement our approach using the mCRL2 model checker, and evaluate it with examples extended from the literature.
Cite as

Adam D. Barwell, Alceste Scalas, Nobuko Yoshida, and Fangyi Zhou. Generalised Multiparty Session Types with Crash-Stop Failures. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 35:1-35:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{barwell_et_al:LIPIcs.CONCUR.2022.35,
  author =	{Barwell, Adam D. and Scalas, Alceste and Yoshida, Nobuko and Zhou, Fangyi},
  title =	{{Generalised Multiparty Session Types with Crash-Stop Failures}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{35:1--35:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.35},
  URN =		{urn:nbn:de:0030-drops-170982},
  doi =		{10.4230/LIPIcs.CONCUR.2022.35},
  annote =	{Keywords: Session Types, Concurrency, Failure Handling, Model Checking}
}
Document
DOI: 10.4230/DagRep.11.8.52
Behavioural Types: Bridging Theory and Practice (Dagstuhl Seminar 21372)

Authors: Mariangiola Dezani, Roland Kuhn, Sam Lindley, and Alceste Scalas

Published in: Dagstuhl Reports, Volume 11, Issue 8 (2022)

Abstract
Behavioural types specify the way in which software components interact with one another. Unlike data types (which describe the structure of data), behavioural types describe communication protocols, and their verification ensures that programs do not violate such protocols. The behavioural types research community has developed a flourishing literature on communication-centric programming, exploring many directions. One of the most studied behavioural type systems are session types, introduced by Honda et al. in the ‘90s, and awarded with prizes for their influence in the past 20 and 10 years (by the ESOP and POPL conferences, respectively). Other varieties of behavioural types include typestate systems, choreographies, and behavioural contracts; research on verification techniques covers the spectrum from fully static verification at compile-time to fully dynamic verification at run-time. In the last decade, research on behavioural types has shifted emphasis towards practical applications, using both novel and existing programming languages (e.g., Java, Python, Go, C, Haskell, OCaml, Erlang, Scala, Rust). An earlier Dagstuhl Seminar, 17051 "Theory and Applications of Behavioural Types" (January 29-February 3, 2017), played an important role in coordinating this effort. Yet, despite the vibrant community and the stream of new results, the use of behavioural types for mainstream software development and verification remains limited. This limitation is largely down to the rapid pace at which mainstream industrial practice for the design and development of concurrent and distributed systems evolves, often resulting in substantial divergence from academic research. In the absence of established tools to express communication protocols, widely used implementations concentrate solely on scalability and reliability. The flip side is that these systems are either overly loose, supporting any conceivable communication structure (via brokers), or overly restricted, supporting only simple request-response protocols (like HTTP or RPC). In this seminar, experts from academia and industry explored together how best to bridge the gap between theory and mainstream practice. They tackled challenges that are fundamental in practical systems development, but are rarely or only partially addressed in the behavioural types literature - in particular, failure handling, asynchronous communication, and dynamic reconfiguration. Moreover they explored how the tools of behavioural types and programming languages theory (such as linearity, gradual types, and dependent types) can help to address these challenges.
Cite as

Mariangiola Dezani, Roland Kuhn, Sam Lindley, and Alceste Scalas. Behavioural Types: Bridging Theory and Practice (Dagstuhl Seminar 21372). In Dagstuhl Reports, Volume 11, Issue 8, pp. 52-75, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{dezani_et_al:DagRep.11.8.52,
  author =	{Dezani, Mariangiola and Kuhn, Roland and Lindley, Sam and Scalas, Alceste},
  title =	{{Behavioural Types: Bridging Theory and Practice (Dagstuhl Seminar 21372)}},
  pages =	{52--75},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2022},
  volume =	{11},
  number =	{8},
  editor =	{Dezani, Mariangiola and Kuhn, Roland and Lindley, Sam and Scalas, Alceste},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.11.8.52},
  URN =		{urn:nbn:de:0030-drops-157699},
  doi =		{10.4230/DagRep.11.8.52},
  annote =	{Keywords: behavioural types, concurrency, programming languages, session types}
}
Document
Artifact
DOI: 10.4230/DARTS.7.2.2
On the Monitorability of Session Types, in Theory and Practice (Artifact)

Authors: Christian Bartolo Burlò, Adrian Francalanza, and Alceste Scalas

Published in: DARTS, Volume 7, Issue 2, Special Issue of the 35th European Conference on Object-Oriented Programming (ECOOP 2021)

Abstract
In the paper "On the Monitorability of Session Types, in Theory and Practice" we study the monitorability of message-passing black-box processes against protocol specifications expressed as session types; we formalise a monitor synthesis procedure, prove its correctness, and discuss its implementation - as a tool that synthesises an executable monitor (in the Scala programming language) from a given session type. This artifact contains the aforementioned monitor synthesis tool, called STMonitor; it includes the tool source code, and documentation to reproduce the examples and benchmarks described in the paper.
Cite as

Christian Bartolo Burlò, Adrian Francalanza, and Alceste Scalas. On the Monitorability of Session Types, in Theory and Practice (Artifact). In Special Issue of the 35th European Conference on Object-Oriented Programming (ECOOP 2021). Dagstuhl Artifacts Series (DARTS), Volume 7, Issue 2, pp. 2:1-2:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@Article{bartoloburlo_et_al:DARTS.7.2.2,
  author =	{Bartolo Burl\`{o}, Christian and Francalanza, Adrian and Scalas, Alceste},
  title =	{{On the Monitorability of Session Types, in Theory and Practice (Artifact)}},
  pages =	{2:1--2:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2021},
  volume =	{7},
  number =	{2},
  editor =	{Bartolo Burl\`{o}, Christian and Francalanza, Adrian and Scalas, Alceste},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.7.2.2},
  URN =		{urn:nbn:de:0030-drops-140267},
  doi =		{10.4230/DARTS.7.2.2},
  annote =	{Keywords: Session types, monitorability, monitor correctness, Scala}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2021.20
On the Monitorability of Session Types, in Theory and Practice

Authors: Christian Bartolo Burlò, Adrian Francalanza, and Alceste Scalas

Published in: LIPIcs, Volume 194, 35th European Conference on Object-Oriented Programming (ECOOP 2021)

Abstract
Software components are expected to communicate according to predetermined protocols and APIs. Numerous methods have been proposed to check the correctness of communicating systems against such protocols/APIs. Session types are one such method, used both for static type-checking as well as for run-time monitoring. This work takes a fresh look at the run-time verification of communicating systems using session types, in theory and in practice. On the theoretical side, we develop a formal model of session-monitored processes. We then use this model to formulate and prove new results on the monitorability of session types, defined in terms of soundness (i.e., whether monitors only flag ill-typed processes) and completeness (i.e., whether all ill-typed processes can be flagged by a monitor). On the practical side, we show that our monitoring theory is indeed realisable: we instantiate our formal model as a Scala toolkit (called STMonitor) for the automatic generation of session monitors. These executable monitors can be used as proxies to instrument communication across black-box processes written in any programming language. Finally, we evaluate the viability of our approach through a series of benchmarks.
Cite as

Christian Bartolo Burlò, Adrian Francalanza, and Alceste Scalas. On the Monitorability of Session Types, in Theory and Practice. In 35th European Conference on Object-Oriented Programming (ECOOP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 194, pp. 20:1-20:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{bartoloburlo_et_al:LIPIcs.ECOOP.2021.20,
  author =	{Bartolo Burl\`{o}, Christian and Francalanza, Adrian and Scalas, Alceste},
  title =	{{On the Monitorability of Session Types, in Theory and Practice}},
  booktitle =	{35th European Conference on Object-Oriented Programming (ECOOP 2021)},
  pages =	{20:1--20:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-190-0},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{194},
  editor =	{M{\o}ller, Anders and Sridharan, Manu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2021.20},
  URN =		{urn:nbn:de:0030-drops-140630},
  doi =		{10.4230/LIPIcs.ECOOP.2021.20},
  annote =	{Keywords: Session types, monitorability, monitor correctness, Scala}
}
Document
DOI: 10.4230/DARTS.3.2.3
A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming (Artifact)

Authors: Alceste Scalas, Ornela Dardha, Raymond Hu, and Nobuko Yoshida

Published in: DARTS, Volume 3, Issue 2, Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017)

Abstract
This artifact contains a version of the Scribble tool that, given a protocol specification with multiple participants, can generate Scala APIs for implementing each participant in a type-safe, protocol-abiding way. Crucially, the API generation leverages a decomposition of the multiparty protocol into type-safe peer-to-peer interactions between pairs of participants; and this, in turn, allows to implement the API internals on top of the existing lchannels library for type-safe binary session programming. As a result, several technically challenging aspects in the implementation of multiparty sessions are solved "for free", at the underlying binary level. This includes distributed multiparty session delegation: this artifact implements it for the first time.
Cite as

Alceste Scalas, Ornela Dardha, Raymond Hu, and Nobuko Yoshida. A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming (Artifact). In Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017). Dagstuhl Artifacts Series (DARTS), Volume 3, Issue 2, pp. 3:1-3:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Article{scalas_et_al:DARTS.3.2.3,
  author =	{Scalas, Alceste and Dardha, Ornela and Hu, Raymond and Yoshida, Nobuko},
  title =	{{A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming (Artifact)}},
  pages =	{3:1--3:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2017},
  volume =	{3},
  number =	{2},
  editor =	{Scalas, Alceste and Dardha, Ornela and Hu, Raymond and Yoshida, Nobuko},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.3.2.3},
  URN =		{urn:nbn:de:0030-drops-72847},
  doi =		{10.4230/DARTS.3.2.3},
  annote =	{Keywords: process calculi, session types, concurrent programming, Scala}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2017.24
A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming

Authors: Alceste Scalas, Ornela Dardha, Raymond Hu, and Nobuko Yoshida

Published in: LIPIcs, Volume 74, 31st European Conference on Object-Oriented Programming (ECOOP 2017)

Abstract
Multiparty Session Types (MPST) is a typing discipline for message-passing distributed processes that can ensure properties such as absence of communication errors and deadlocks, and protocol conformance. Can MPST provide a theoretical foundation for concurrent and distributed programming in "mainstream" languages? We address this problem by (1) developing the first encoding of a full-fledged multiparty session pi-calculus into linear pi-calculus, and (2) using the encoding as the foundation of a practical toolchain for safe multiparty programming in Scala. Our encoding is type-preserving and operationally sound and complete. Crucially, it keeps the distributed choreographic nature of MPST, illuminating that the safety properties of multiparty sessions can be precisely represented with a decomposition into binary linear channels. Previous works have only studied the relation between (limited) multiparty and binary sessions via centralised orchestration means. We exploit these results to implement an automated generation of Scala APIs for multiparty sessions, abstracting existing libraries for binary communication channels. This allows multiparty systems to be safely implemented over binary message transports, as commonly found in practice. Our implementation is the first to support distributed multiparty delegation: our encoding yields it for free, via existing mechanisms for binary delegation.
Cite as

Alceste Scalas, Ornela Dardha, Raymond Hu, and Nobuko Yoshida. A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 24:1-24:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{scalas_et_al:LIPIcs.ECOOP.2017.24,
  author =	{Scalas, Alceste and Dardha, Ornela and Hu, Raymond and Yoshida, Nobuko},
  title =	{{A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming}},
  booktitle =	{31st European Conference on Object-Oriented Programming (ECOOP 2017)},
  pages =	{24:1--24:31},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-035-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{74},
  editor =	{M\"{u}ller, Peter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.24},
  URN =		{urn:nbn:de:0030-drops-72637},
  doi =		{10.4230/LIPIcs.ECOOP.2017.24},
  annote =	{Keywords: process calculi, session types, concurrent programming, Scala}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2016.21
Lightweight Session Programming in Scala

Authors: Alceste Scalas and Nobuko Yoshida

Published in: LIPIcs, Volume 56, 30th European Conference on Object-Oriented Programming (ECOOP 2016)

Abstract
Designing, developing and maintaining concurrent applications is an error-prone and time-consuming task; most difficulties arise because compilers are usually unable to check whether the inputs/outputs performed by a program at runtime will adhere to a given protocol specification. To address this problem, we propose lightweight session programming in Scala: we leverage the native features of the Scala type system and standard library, to introduce (1) a representation of session types as Scala types, and (2) a library, called lchannels, with a convenient API for session-based programming, supporting local and distributed communication. We generalise the idea of Continuation-Passing Style Protocols (CPSPs), studying their formal relationship with session types. We illustrate how session programming can be carried over in Scala: how to formalise a communication protocol, and represent it using Scala classes and lchannels, letting the compiler help spotting protocol violations. We attest the practicality of our approach with a complex use case, and evaluate the performance of lchannels with a series of benchmarks.
Cite as

Alceste Scalas and Nobuko Yoshida. Lightweight Session Programming in Scala. In 30th European Conference on Object-Oriented Programming (ECOOP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 56, pp. 21:1-21:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{scalas_et_al:LIPIcs.ECOOP.2016.21,
  author =	{Scalas, Alceste and Yoshida, Nobuko},
  title =	{{Lightweight Session Programming in Scala}},
  booktitle =	{30th European Conference on Object-Oriented Programming (ECOOP 2016)},
  pages =	{21:1--21:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-014-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{56},
  editor =	{Krishnamurthi, Shriram and Lerner, Benjamin S.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2016.21},
  URN =		{urn:nbn:de:0030-drops-61156},
  doi =		{10.4230/LIPIcs.ECOOP.2016.21},
  annote =	{Keywords: session types, Scala, concurrency}
}
Document
DOI: 10.4230/DARTS.2.1.11
Lightweight Session Programming in Scala (Artifact)

Authors: Alceste Scalas and Nobuko Yoshida

Published in: DARTS, Volume 2, Issue 1, Special Issue of the 30th European Conference on Object-Oriented Programming (ECOOP 2016)

Abstract
In the paper "Lightweight Session Programming in Scala", we introduce a "lightweight" integration of session types in the Scala programming language, based on (1) a formal type-level encoding, and (2) a library implementation of linear I/O channels, called lchannels, providing a convenient API for session-based programming, and supporting both local and distributed communication. This artifact is the source code of lchannels, with all the examples and benchmarks discussed in the paper.
Cite as

Alceste Scalas and Nobuko Yoshida. Lightweight Session Programming in Scala (Artifact). In Special Issue of the 30th European Conference on Object-Oriented Programming (ECOOP 2016). Dagstuhl Artifacts Series (DARTS), Volume 2, Issue 1, pp. 11:1-11:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@Article{scalas_et_al:DARTS.2.1.11,
  author =	{Scalas, Alceste and Yoshida, Nobuko},
  title =	{{Lightweight Session Programming in Scala (Artifact)}},
  pages =	{11:1--11:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2016},
  volume =	{2},
  number =	{1},
  editor =	{Scalas, Alceste and Yoshida, Nobuko},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.2.1.11},
  URN =		{urn:nbn:de:0030-drops-61327},
  doi =		{10.4230/DARTS.2.1.11},
  annote =	{Keywords: session types, Scala, concurrency}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact